Skip to content

Minor java loading changes to support alternative loading strategies #5107

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom
Merged
merged 1 commit into from
Sep 23, 2019
Merged

Minor java loading changes to support alternative loading strategies #5107

merged 1 commit into from
Sep 23, 2019

Conversation

thomasspriggs
Copy link
Contributor

@thomasspriggs thomasspriggs commented Sep 13, 2019 •
edited
Loading

These minor changes to loading interfaces in a couple of places support the use of alternative loading strategies in downstream repositories.

  • Each commit message has a non-empty body, explaining why the change was made.
  • Methods or procedures I have added are documented, following the guidelines provided in CODING_STANDARD.md.
  • The feature or user visible behaviour I have added or modified has been documented in the User Guide in doc/cprover-manual/
  • Regression or unit tests are included, or existing tests cover the modified code (in this case I have detailed which ones those are in the commit message).
  • My commit message includes data points confirming performance improvements (if claimed).
  • My PR is restricted to a single feature or bugfix.
  • White-space or formatting changes outside the feature-related changed lines are in commits of their own.

thk123
thk123 approved these changes Sep 13, 2019
View reviewed changes
src/goto-programs/lazy_goto_model.h Outdated
@@ -243,6 +243,12 @@ class lazy_goto_modelt : public abstract_goto_modelt
return goto_functions.at(id);
}

goto_functionst::goto_functiont &get_goto_function_writable(
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

⛏️ Given your commit message:

place entirely before symex it's ok if you're careful.

Probably worth doxygen comment explaining this danger (and if possible a check that symex hasn't begun??)

owen-mc-diffblue
owen-mc-diffblue approved these changes Sep 13, 2019
View reviewed changes
Copy link
Contributor

@owen-mc-diffblue owen-mc-diffblue left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

You should add the comment Thomas asked for

@jeannielynnmoulton jeannielynnmoulton removed their request for review September 16, 2019 13:24
@smowton @thomasspriggs
Make symbol table refs const
22dc0f5 
These never needed to be mutable. Making them const means that they
can be used from contexts where the symbol table is const.
@thomasspriggs thomasspriggs force-pushed the tas/alternative-loading-compatibility-minimal branch 2 times, most recently from e2ee53b to 74aa09b Compare September 20, 2019 10:05
@codecov-io
Copy link

codecov-io commented Sep 20, 2019 •
edited
Loading

Codecov Report

Merging #5107 into develop will not change coverage.
The diff coverage is n/a.

Impacted file tree graph

@@           Coverage Diff            @@
##           develop    #5107   +/-   ##
========================================
  Coverage    66.95%   66.95%           
========================================
  Files         1145     1145           
  Lines        93650    93650           
========================================
  Hits         62699    62699           
  Misses       30951    30951
Flag Coverage Δ
#cproversmt2 42.68% <ø> (ø) ⬆️
#regression 63.44% <ø> (ø) ⬆️
#unit 31.7% <ø> (ø) ⬆️
Impacted Files Coverage Δ
src/goto-programs/lazy_goto_model.h 90.47% <ø> (ø) ⬆️
jbmc/src/java_bytecode/ci_lazy_methods_needed.h 100% <ø> (ø) ⬆️
src/goto-programs/lazy_goto_functions_map.h 100% <0%> (ø) ⬆️

Continue to review full report at Codecov.

Legend - Click here to learn more
Δ = absolute <relative> (impact), ø = not affected, ? = missing data
Powered by Codecov. Last update 20164f5...74aa09b. Read the comment docs.

allredj
allredj reviewed Sep 20, 2019
View reviewed changes
Copy link
Contributor

@allredj allredj left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

✔️
Passed Diffblue compatibility checks (cbmc commit: 74aa09b).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/128496241

@thomasspriggs thomasspriggs force-pushed the tas/alternative-loading-compatibility-minimal branch from 74aa09b to 22dc0f5 Compare September 23, 2019 15:04
@thomasspriggs
Copy link
Contributor Author

I have now removed the second commit from this PR, as the code which needs a writable reference to a goto function should be called from the process_goto_functions member function instead. This function already has access to a non-const goto_modelt. Therefore access to mutate functions through a lazy_goto_modelt is no longer required.

allredj
allredj reviewed Sep 23, 2019
View reviewed changes
Copy link
Contributor

@allredj allredj left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

✔️
Passed Diffblue compatibility checks (cbmc commit: 22dc0f5).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/128785171

@thomasspriggs thomasspriggs merged commit 1b94092 into diffblue:develop Sep 23, 2019
@thomasspriggs thomasspriggs deleted the tas/alternative-loading-compatibility-minimal branch September 23, 2019 18:13
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@allredj allredj allredj left review comments

@smowton smowton smowton approved these changes

@thk123 thk123 thk123 approved these changes

@owen-mc-diffblue owen-mc-diffblue owen-mc-diffblue approved these changes

@cesaro cesaro Awaiting requested review from cesaro

@cristina-david cristina-david Awaiting requested review from cristina-david

@kroening kroening Awaiting requested review from kroening

@NathanJPhillips NathanJPhillips Awaiting requested review from NathanJPhillips

@peterschrammel peterschrammel Awaiting requested review from peterschrammel peterschrammel is a code owner

@pkesseli pkesseli Awaiting requested review from pkesseli

@tautschnig tautschnig Awaiting requested review from tautschnig

@antlechner antlechner Awaiting requested review from antlechner

Assignees
No one assigned
Labels
None yet
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.
6 participants
@thomasspriggs @codecov-io @smowton @thk123 @allredj @owen-mc-diffblue